Nuprl Lemma : detach_fun_properties 13,42

T:Type, A:(T), d:detach_fun(T;A). {x:T. ((A(x)))  ((d(x)))} 
latex


Upgen algebra 1
Definitions of Statementdetach_fun(T;A)
Definitionst  T, {T}, , x:AB(x), True, P  Q, P & Q, xt(x), P  Q, T, P  Q, detach_fun(T;A), x(s), SqStable(P)
Lemmasdetach fun wf, sq stable squash, decidable assert, sq stable from decidable, sq stable implies, rev implies wf, sq stable and, assert wf, squash wf, iff wf, sq stable all

origin